/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓re: Joseph Weening

␈↓ α∧␈↓␈↓ αTJoe␈α
Weening␈α
is␈α
strongly␈α
motivated␈α
to␈α
be␈α
immediately␈α
helpful,␈α
sometimes␈α
at␈α
the␈α
cost␈α
of␈α
his
␈↓ α∧␈↓long term interests.

␈↓ α∧␈↓␈↓ αTWhile he has been my research and teaching assistant he has done the following:

␈↓ α∧␈↓1.␈α
He␈αhas␈α
taken␈α
charge␈αof␈α
the␈αmanual␈α
for␈α
Jussi␈αKetonen's␈α
interactive␈αtheorem␈α
prover␈α
EKL.␈α He
␈↓ α∧␈↓has␈αwritten␈αseveral␈α
versions␈αof␈αthe␈αmanual,␈α
keeping␈αup␈αwith␈αall␈α
the␈αchanges.␈α This␈αmanual␈α
is␈αan
␈↓ α∧␈↓absolutely first class job of clear exposition.  I have never had a student who writes as well as Joe.

␈↓ α∧␈↓2.␈α∞He␈α∞has␈α∞done␈α∞the␈α∞parser␈α∞for␈α∞EKL.␈α∞ This␈α∞is␈α∞an␈α∞excellent␈α∞job,␈α∞but␈α∞so␈α∞far␈α∞as␈α∞I␈α∞know,␈α∞it␈α
doesn't
␈↓ α∧␈↓contain␈α∂new␈α∞ideas.␈α∂ Unlike␈α∂the␈α∞parsers␈α∂of␈α∞my␈α∂previous␈α∂experience,␈α∞it␈α∂doesn't␈α∞seem␈α∂to␈α∂have␈α∞any
␈↓ α∧␈↓bugs even though the syntax allowed is quite rich.  It doesn't give mysterious syntax errors.

␈↓ α∧␈↓3.␈αHe␈αhas␈αmade␈αseveral␈αsmall␈αimprovements␈αto␈αthe␈αoperating␈αsystem,␈αand␈αhe␈αis␈αone␈αof␈αthe␈αpeople
␈↓ α∧␈↓who␈αfixes␈αit␈αwhen␈αit␈αbreaks.␈α This␈αis␈αnot␈αpart␈αof␈αhis␈αjob.␈α When␈αJoe␈αsees␈αsomething␈αthat␈αneeds␈αto
␈↓ α∧␈↓be done, he has a tendency to go ahead and do it.

␈↓ α∧␈↓4.␈αHe␈αhas␈αalso␈αbeen␈α
one␈αof␈αthe␈αleaders␈αof␈αthe␈α
graduate␈αstudents␈αof␈αthe␈αStanford␈αComputer␈α
Science
␈↓ α∧␈↓Department - again part of his tendency to take charge of what he sees needs to be done.

␈↓ α∧␈↓␈↓ αTJoe␈α∞has␈α∞undertaken␈α
to␈α∞do␈α∞a␈α∞thesis␈α
involving␈α∞a␈α∞practical␈α
system␈α∞for␈α∞proving␈α∞correctness␈α
of
␈↓ α∧␈↓LISP␈α⊂programs.␈α∂ If␈α⊂he␈α⊂succeeds,␈α∂he␈α⊂will␈α⊂unprecedentedly␈α∂combine␈α⊂theoretical␈α⊂understanding␈α∂of
␈↓ α∧␈↓program␈α
semantics␈α
with␈α
the␈α
ability␈α
to␈α
build␈α
practical␈α
systems.␈α
 From␈α
my␈α
point␈α
of␈α
view,␈α
he␈α
has␈α
been
␈↓ α∧␈↓somewhat␈α∂slow␈α∂in␈α∂getting␈α∂started␈α∂in␈α∂his␈α∂theoretical␈α∂work.␈α∂ However,␈α∂hardly␈α∂any␈α∂theorists␈α∞really
␈↓ α∧␈↓want␈αto␈αbuild␈αuseful␈αsystems,␈αand␈αJoe␈αcertainly␈αdoes.␈α Therefore,␈αI␈αconsider␈αthat␈αhe␈αis␈αthe␈αbest␈αbet
␈↓ α∧␈↓yet to do genuinely useful work in program verification.

␈↓ α∧␈↓␈↓ αTCompared␈α∪to␈α∩the␈α∪Hertz␈α∩fellows␈α∪I␈α∪know,␈α∩Mike␈α∪Farmwald,␈α∩Tom␈α∪McWilliams␈α∪and␈α∩Kurt
␈↓ α∧␈↓Widdoes,␈α∞Joe␈α∞Weening␈α∞is␈α∞of␈α∞equal␈α∞ability␈α∞but␈α∞more␈α∞theoretically␈α∞oriented.␈α∞ He␈α∞also␈α∞shares␈α
their
␈↓ α∧␈↓interest in useful products.

␈↓ α∧␈↓␈↓ αTCompared␈αto␈αthe␈αbetter␈αstudents␈αin␈αthe␈αComputer␈αScience␈αDepartment,␈αJoe␈αis␈αnot␈α
as␈αstrong
␈↓ α∧␈↓in␈α⊂theory␈α⊂as␈α⊂the␈α⊂best␈α⊂theorists.␈α⊂ He␈α∂hasn't␈α⊂yet␈α⊂written␈α⊂any␈α⊂theoretical␈α⊂papers␈α⊂-␈α⊂perhaps␈α∂partly
␈↓ α∧␈↓because␈αI␈αhaven't␈αdemanded␈αit.␈α He␈αis␈αup␈αthere␈αwith␈αthe␈αbest␈αpractical␈αsystem␈αbuilders,␈αand␈αhe␈αis
␈↓ α∧␈↓strong␈αenough␈α
on␈αtheory␈α
so␈αthat␈α
there␈αis␈α
a␈αgood␈αchance␈α
that␈αis␈α
project␈αwill␈α
be␈αboth␈α
a␈αtheoretical
␈↓ α∧␈↓and a practical success.  This is very rare indeed.

␈↓ α∧␈↓␈↓ αTFor these reasons I recommend him strongly.